$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $x$, $y$:$A$, $v$:Top. $x$ $\in$ dom($y$ : $v$) $\Leftrightarrow$ $x$ $=$ $y$